Nuprl Definition : Q-R-pre-preserving
11,40
postcript
pdf
f
is
Q
-
R
-pre-preserving on
P
==
e
,
e'
:{
e
:E|
P
(
e
)} . (
Q
(
f
(
e
),
f
(
e'
)))
(
R
(
e
,
e'
))
latex
clarification:
Q-R-pre-preserving(
es
;
f
;
P
;
Q
;
R
)
==
e
:{
e
:es-E(
es
)|
P
(
e
)} ,
e'
:{
e
:es-E(
es
)|
P
(
e
)} . (
Q
(
f
(
e
),
f
(
e'
)))
(
R
(
e
,
e'
))
latex
Definitions
x
:
A
.
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
E
,
P
Q
,
f
(
a
)
FDL editor aliases
Q-R-pre-preserving
origin